Nuprl Lemma : mkfpf_wf
0,22
postcript
pdf
A
:Type,
a
:
A
List,
b
:({
a@0
:
A
| (
a@0
a
) }
Top). mkfpf(
a
;
b
)
a
:
A
fp
Top
latex
Definitions
a
:
A
fp
B
(
a
)
,
mkfpf(
a
;
b
)
,
(
x
l
)
,
x
:
A
.
B
(
x
)
,
Top
,
t
T
Lemmas
top
wf
,
l
member
wf
origin
A:Type, a:A List, b:({a@0:A| (a@0 
a) }
Top). mkfpf(a;b) a:A fp Top A:Type, a:A List, b:({a@0:A| (a@0 a) }Top). mkfpf(a;b) a:A fp Top B(a) l)x:A. B(x) T